(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x45AA8665D7B3D31C) #x0000000000000000))
(constraint (= (f #xA568F608633F9298) #x0000000000000000))
(constraint (= (f #xD46C5E33671A14DC) #x0000000000000000))
(constraint (= (f #x1CB5F0230AFF2192) #x0000000000000000))
(constraint (= (f #xEB1A14966159EE58) #x0000000000000000))
(constraint (= (f #x112A0D5620193E5A) #x0000000000000000))
(constraint (= (f #x207D200467198A3C) #x0000000000000000))
(constraint (= (f #xDCD0322888311CD0) #x0000000000000000))
(constraint (= (f #x48E9314C281146F2) #x0000000000000000))
(constraint (= (f #xA2C5118A241124F6) #x0000000000000000))
(constraint (= (f #x000888889999999C) #x0000000000000000))
(constraint (= (f #x000088888899BFFE) #x0000000000000000))
(constraint (= (f #x0000000089BBFFFE) #x0000000000000000))
(constraint (= (f #x88888CCCDDDDDDDC) #x0000000000000000))
(constraint (= (f #x044444CCCDDDDDDC) #x0000000000000000))
(constraint (= (f #x1EC186BAEF42F096) #x0000000000000000))
(constraint (= (f #x4FF29BBD0D46D9BE) #x0000000000000000))
(constraint (= (f #xBDC86B3604ECAE38) #x0000000000000000))
(constraint (= (f #xCA744F301E6C4B1A) #x0000000000000000))
(constraint (= (f #xB9721A7BFFA6661C) #x0000000000000000))
(constraint (= (f #x6A9F7BA41A74C240) #xD53EF74834E98480))
(constraint (= (f #x4FAC4EEB1A1B5BAC) #x9F589DD63436B758))
(constraint (= (f #xAD76A0C57114AF8A) #x5AED418AE2295F14))
(constraint (= (f #x31974AD67C300602) #x632E95ACF8600C04))
(constraint (= (f #x3397D71AAEFF4662) #x672FAE355DFE8CC4))
(constraint (= (f #x2D9BE67E1BE2F56B) #x0000423608E03540))
(constraint (= (f #x7C65DA2D3787D5E5) #x0000D80934024504))
(constraint (= (f #x1CB67F78708081E7) #x0000396870808100))
(constraint (= (f #x25DAD0F370CCA3A5) #x000040B120C4A180))
(constraint (= (f #xBB28CE789E069C21) #x000046509C001C00))
(constraint (= (f #x36089B6008E371D4) #x0000000000000000))
(constraint (= (f #xE3114088E341C090) #x0000000000000000))
(constraint (= (f #x13DC421080A5F53C) #x0000000000000000))
(constraint (= (f #x12B894102C4D0832) #x0000000000000000))
(constraint (= (f #xFE101C4E2A0D4730) #x0000000000000000))
(constraint (= (f #x000006666666EFFE) #x00000CCCCCCDDFFC))
(constraint (= (f #x0000000000033376) #x00000000000666EC))
(constraint (= (f #x466666666667777E) #x8CCCCCCCCCCEEEFC))
(constraint (= (f #x002AAAAAEEEEEEFE) #x00555555DDDDDDFC))
(constraint (= (f #x000000008888899A) #x0000000111111334))
(constraint (= (f #x1645F404F966C6A8) #x2C8BE809F2CD8D50))
(constraint (= (f #x4AAC48EB1189CA84) #x955891D623139508))
(constraint (= (f #x03F42448A162EC2C) #x07E8489142C5D858))
(constraint (= (f #x9DBF0B915A0094A0) #x3B7E1722B4012940))
(constraint (= (f #xAA4DD38CEA4FCD86) #x549BA719D49F9B0C))
(constraint (= (f #x544281E02A5912EF) #x00008080024010A2))
(constraint (= (f #x9A7B864A23B723E1) #x0001044200940360))
(constraint (= (f #xEBA0B335899C0AC7) #x0000930100080200))
(constraint (= (f #xB3EC4FA7A353E82B) #x0000478083434022))
(constraint (= (f #x6098714AECBE2949) #x00004100E0940948))
(constraint (= (f #x3C19A7BDF2C522B5) #x78334F7BE58A456A))
(constraint (= (f #xB0D687322EAFB0DF) #x61AD0E645D5F61BE))
(constraint (= (f #x0C43B2EB11871E97) #x188765D6230E3D2E))
(constraint (= (f #x95B91D1914C7E31F) #x2B723A32298FC63E))
(constraint (= (f #xA7D3CB5599ACE399) #x4FA796AB3359C732))
(constraint (= (f #x00000000000177FE) #x0000000000000000))
(constraint (= (f #x0000000000011DDC) #x0000000000000000))
(constraint (= (f #x00000000000199BA) #x0000000000000000))
(constraint (= (f #x00000000000117FE) #x0000000000000000))
(constraint (= (f #x00000000000113BE) #x0000000000000000))
(constraint (= (f #x0A86439302030C95) #x0000000000000000))
(constraint (= (f #x60D970084C232019) #x0000000000000000))
(constraint (= (f #x2A31488346419A17) #x0000000000000000))
(constraint (= (f #x7418AE540A830155) #x0000000000000000))
(constraint (= (f #x02274881432BC517) #x0000000000000000))
(constraint (= (f #xB54E25374EB080F9) #x6A9C4A6E9D6101F2))
(constraint (= (f #x180119EFEDFA55FD) #x300233DFDBF4ABFA))
(constraint (= (f #xF7F4FC201B529EBF) #xEFE9F84036A53D7E))
(constraint (= (f #xDF9446364550CA19) #xBF288C6C8AA19432))
(constraint (= (f #xEB61D02D8AFF0CB3) #xD6C3A05B15FE1966))
(constraint (= (f #x09E26118E03184F7) #x0000000000000000))
(constraint (= (f #x0529092A44593237) #x0000000000000000))
(constraint (= (f #x88051AA60417A29D) #x0000000000000000))
(constraint (= (f #x3D082938085B3A5B) #x0000000000000000))
(constraint (= (f #x6B4008D202DF9013) #x0000000000000000))
(constraint (= (f #x0C488862762E9D22) #x189110C4EC5D3A44))
(constraint (= (f #xF78C08FCB2A6ECE9) #x0000081810A06448))
(constraint (= (f #x38A2CB1E9AB7EBE7) #x0000410492352166))
(constraint (= (f #xE5E1D8558611C033) #xCBC3B0AB0C238066))
(constraint (= (f #x8DB899BC3F067328) #x1B7133787E0CE650))
(constraint (= (f #xF39FCAC10422E134) #x0000000000000000))
(constraint (= (f #x67E1465076C81B51) #xCFC28CA0ED9036A2))
(constraint (= (f #x199D8CF45416DA3A) #x0000000000000000))
(constraint (= (f #xD6330D29A9D64E9E) #x0000000000000000))
(constraint (= (f #xB1272203F6ED3E31) #x624E4407EDDA7C62))
(constraint (= (f #xC281C1A2C081C7D1) #x0000000000000000))
(constraint (= (f #xFD01F7738799F288) #xFA03EEE70F33E510))
(constraint (= (f #xEAB1040588257D17) #x0000000000000000))
(constraint (= (f #xC27C1EC33CAFB395) #x84F83D86795F672A))
(constraint (= (f #x6E27518F53A577BB) #xDC4EA31EA74AEF76))
(constraint (= (f #x90D0A0D1026F5819) #x0000000000000000))
(constraint (= (f #xF53AF300B9679219) #xEA75E60172CF2432))
(constraint (= (f #x39000B020415B2B3) #x0000000000000000))
(constraint (= (f #x43663B828777925B) #x86CC77050EEF24B6))
(constraint (= (f #x4BD16B00CF3C69B1) #x97A2D6019E78D362))
(constraint (= (f #x7B300CFC0019C81D) #x0000000000000000))
(constraint (= (f #xD3288754E970E8BF) #xA6510EA9D2E1D17E))
(constraint (= (f #x977CC2485CF1289D) #x2EF98490B9E2513A))
(constraint (= (f #x654FF30CC451E5F7) #xCA9FE61988A3CBEE))
(constraint (= (f #x000000000001BBFE) #x0000000000000000))
(constraint (= (f #x222AAAAAAAAAAABA) #x4455555555555574))
(constraint (= (f #x000000000001408A) #x0000000000028114))
(constraint (= (f #x60A1D580073B0853) #x0000000000000000))
(constraint (= (f #x47FC973018DBB5BD) #x8FF92E6031B76B7A))
(constraint (= (f #xF5164ED667C37600) #xEA2C9DACCF86EC00))
(constraint (= (f #x5C0F8B66C13CD4B7) #xB81F16CD8279A96E))
(constraint (= (f #x7864796628BD68F1) #xF0C8F2CC517AD1E2))
(constraint (= (f #x6A0F87AF78F3D757) #xD41F0F5EF1E7AEAE))
(constraint (= (f #x5EBCBF60761F1E97) #xBD797EC0EC3E3D2E))
(constraint (= (f #xB024B1308497929F) #x0000000000000000))
(constraint (= (f #x24E9264732CF1559) #x49D24C8E659E2AB2))
(constraint (= (f #x2A8295512AA5F60E) #x55052AA2554BEC1C))
(constraint (= (f #xD75E603399CBBC97) #xAEBCC0673397792E))
(constraint (= (f #x184E4A0301016BBF) #x0000000000000000))
(constraint (= (f #x68772834E3258AD3) #xD0EE5069C64B15A6))
(constraint (= (f #x0FEACF48A3636295) #x1FD59E9146C6C52A))
(constraint (= (f #xA8124889554428B4) #x0000000000000000))
(constraint (= (f #x000000000000155C) #x0000000000002AB8))
(constraint (= (f #x90955095080A5532) #x0000000000000000))
(constraint (= (f #xA4454A0A248928BB) #x488A941449125176))
(constraint (= (f #x03233AACE703D4FA) #x0000000000000000))
(constraint (= (f #x252A5492A142913E) #x0000000000000000))
(constraint (= (f #xA8952A844A4A92B2) #x0000000000000000))
(constraint (= (f #x00000000000125F7) #x0000000000000000))
(constraint (= (f #x9425088848884939) #x284A111091109272))
(constraint (= (f #x0666666666677776) #x0CCCCCCCCCCEEEEC))
(constraint (= (f #x510FF776098D709C) #x0000000000000000))
(constraint (= (f #x9E3E43F8B80D689E) #x0000000000000000))
(constraint (= (f #x422A1250540A94BE) #x0000000000000000))
(constraint (= (f #x2BE33A266EAA4CBA) #x0000000000000000))
(constraint (= (f #x4E116D522B4C1E34) #x0000000000000000))
(constraint (= (f #xF101E86EEA6F3BF0) #x0000000000000000))
(constraint (= (f #x949C3FF2F96A0736) #x0000000000000000))
(constraint (= (f #xB50085ACAA4B1276) #x0000000000000000))
(constraint (= (f #x000000177777FFFE) #x0000000000000000))
(constraint (= (f #x011111111199BBFE) #x0000000000000000))
(constraint (= (f #x0888CCCCCCCCCDDC) #x1111999999999BB8))
(constraint (= (f #x00000CCDDDDDDDDC) #x0000000000000000))
(constraint (= (f #x46666666667777FE) #x0000000000000000))
(constraint (= (f #x0055555555555556) #x0000000000000000))
(constraint (= (f #x001111111111113A) #x0000000000000000))
(constraint (= (f #x000000011333333A) #x0000000000000000))
(constraint (= (f #x9F00CFF6E5B6C901) #x00000E0085A4C900))
(constraint (= (f #x01C930B56020FE27) #x000000906020C000))
(constraint (= (f #x8012541F7099EA94) #x0000000000000000))
(constraint (= (f #x890EE1EBCCE683AB) #x00000009C0C68188))
(constraint (= (f #x5492A2952514103B) #xA925452A4A282076))
(constraint (= (f #x030C0A2F45012AF4) #x0000000000000000))
(constraint (= (f #xA0B43498827598B2) #x0000000000000000))
(constraint (= (f #xEEEEEEEEEEEEFFFE) #xDDDDDDDDDDDDFFFC))
(check-synth)
